Skip to content

perf: give currRecDepth its own ReaderT layer in CoreM - #14970

Draft
Kha wants to merge 1 commit into
masterfrom
core-recdepth-readert
Draft

perf: give currRecDepth its own ReaderT layer in CoreM #14970
Kha wants to merge 1 commit into
masterfrom
core-recdepth-readert

Conversation

@Kha

@Kha Kha commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR stops the recursion-depth guard from rebuilding Core.Context on every recursive step. Roughly 96% of Core.Context reconstructions exist only to bump the depth counter, and each one paid a reference count increment per pointer field. -0.77%/-1.10% Mathlib/core instrs, -0.55%/-2.88% wall-clock.

withReader can never reuse the Context record, so keeping currRecDepth there made every withIncRecDepth rebuild it. As its own reader layer the depth is just an extra argument, so a recursion step neither allocates nor touches a reference count. The layer sits inside the Context reader so that a bare read still resolves to Context, and CoreM.run gains an initial-depth parameter so nested command elaboration keeps inheriting its caller's depth.

@Kha

Kha commented Aug 29, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for f409edb against 696e847 are in. There are significant results. @Kha

  • ✅ build//instructions: -33.7G (-0.30%)

Large changes (6🟥)

  • 🟥 size/all/.c//lines: +79.5k (+0.65%)
  • 🟥 size/all/.ir//bytes: +3MiB (+0.73%)
  • 🟥 size/all/.olean.private//bytes: +8MiB (+0.60%)
  • 🟥 size/compile/.out//bytes: +25MiB (+0.90%)
  • 🟥 size/install//bytes: +20MiB (+0.64%)
  • 🟥 size/libleanshared.so//bytes: +4MiB (+1.73%)

Medium changes (11✅, 1🟥)

  • ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.2G (-1.07%)
  • ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -1.5G (-0.70%)
  • ✅ elab/big_do//instructions: -92.4M (-0.51%)
  • ✅ elab/big_omega_MT//instructions: -178.9M (-0.91%)
  • ✅ elab/cbv_arm_ldst//instructions: -626.6M (-1.16%)
  • ✅ elab/cbv_system_f//instructions: -1.1G (-1.20%)
  • ✅ elab/grind_bitvec2//instructions: -2.1G (-1.28%)
  • ✅ elab/grind_list2//instructions: -550.9M (-1.42%)
  • 🟥 elab/lift_lets_dag//instructions: +107.5M (+0.89%)
  • ✅ elab/simp_bubblesort_256//instructions: -227.2M (-2.33%)
  • ✅ elab/whnfMatcherImplicitTransparencyCaching//instructions: -120.0M (-0.49%)
  • ✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.2G (-1.14%)

Small changes (490✅, 175🟥)

  • ✅ build/module/Init.BinderPredicates//instructions: -17.7M (-0.84%)
  • ✅ build/module/Init.CbvSimproc//instructions: -15.6M (-0.75%)
  • ✅ build/module/Init.Control.Basic//instructions: -23.9M (-1.11%)
  • ✅ build/module/Init.Control.Except//instructions: -12.3M (-0.87%)
  • ✅ build/module/Init.Control.Lawful.Basic//instructions: -19.6M (-0.92%)
  • ✅ build/module/Init.Control.Lawful.Instances//instructions: -85.2M (-1.28%)
  • ✅ build/module/Init.Conv//instructions: -27.6M (-0.74%)
  • ✅ build/module/Init.Core//instructions: -93.4M (-0.95%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.Attach//instructions: -132.9M (-1.31%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.Basic//instructions: -105.9M (-0.99%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.BinSearch//instructions: -32.5M (-0.55%)
  • ✅ build/module/Init.Data.Array.Bootstrap//instructions: -21.2M (-0.92%)
  • ✅ build/module/Init.Data.Array.Count//instructions: -28.9M (-1.06%)
  • ✅ build/module/Init.Data.Array.DecidableEq//instructions: -25.5M (-1.11%)
  • ✅ build/module/Init.Data.Array.Erase//instructions: -80.2M (-1.14%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.Extract//instructions: -238.1M (-0.71%)
  • ✅ build/module/Init.Data.Array.Find//instructions: -136.1M (-1.41%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.InsertIdx//instructions: -18.9M (-0.72%)
  • ✅ build/module/Init.Data.Array.Lemmas//instructions: -599.3M (-1.15%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -140.8M (-1.49%) (reduced significance based on absolute threshold)
  • and 645 more

@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 29, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 696e847a6c079637186e492f37e22dedf4faf679 --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-29 16:48:07)
  • 💥 Mathlib branch lean-pr-testing-14970 build failed against this PR. (2026-08-29 20:22:48) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c8e19cca2547a89c3aba401afaab9a8808f490a2 --onto 138ca9f20763523c4093baa092cf371e89535098. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-31 17:25:16)

@leanprover-bot

leanprover-bot commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 696e847a6c079637186e492f37e22dedf4faf679 --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force reference manual CI using the force-manual-ci label. (2026-08-29 16:48:08)
  • ✅ Reference manual branch lean-pr-testing-14970 has successfully built against this PR. (2026-08-29 20:19:59) View Log
  • 🟡 Reference manual branch lean-pr-testing-14970 build against this PR didn't complete normally. (2026-08-29 20:21:10) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c8e19cca2547a89c3aba401afaab9a8808f490a2 --onto e991a05e359a25988f49bff3ab8af986e959b866. You can force reference manual CI using the force-manual-ci label. (2026-08-31 17:25:19)

@Kha
Kha force-pushed the core-recdepth-readert branch from f409edb to f51ba22 Compare August 29, 2026 19:50
@Kha

Kha commented Aug 29, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for f51ba22 against e991a05 are in. There are significant results. @Kha

  • ✅ build//instructions: -88.5G (-0.77%)

Large changes (2✅, 5🟥)

  • ✅ elab/big_do//instructions: -183.1M (-0.99%)
  • ✅ elab/grind_bitvec2//task-clock: -9s (-27.77%)
  • 🟥 size/all/.c//lines: +80.3k (+0.66%)
  • 🟥 size/all/.ir//bytes: +3MiB (+0.73%)
  • 🟥 size/compile/.out//bytes: +24MiB (+0.87%)
  • 🟥 size/install//bytes: +20MiB (+0.64%)
  • 🟥 size/libleanshared.so//bytes: +4MiB (+1.71%)

Medium changes (30✅, 2🟥)

  • ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.9G (-1.67%)
  • ✅ build/module/Init.Data.SInt.Lemmas//instructions: -1.0G (-1.85%)
  • ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.3G (-1.06%)
  • ✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -1.2G (-1.79%)
  • ✅ build/module/Std.Data.HashMap.RawLemmas//instructions: -2.3G (-2.43%)
  • ✅ build/module/Std.Data.Internal.List.Associative//instructions: -1.3G (-1.62%)
  • ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -1.1G (-1.33%)
  • ✅ build/profile/elaboration//wall-clock: -12s (-5.49%)
  • ✅ build/profile/simp//wall-clock: -11s (-8.55%)
  • ✅ elab/big_match_partial//instructions: -210.5M (-1.53%)
  • ✅ elab/big_omega//instructions: -275.8M (-1.39%)
  • ✅ elab/big_omega_MT//instructions: -295.3M (-1.48%)
  • ✅ elab/bv_stress_structures_2//instructions: -352.7M (-1.87%)
  • ✅ elab/cbv_arm_ldst//instructions: -1.0G (-1.87%)
  • ✅ elab/cbv_system_f//instructions: -1.7G (-1.86%)
  • ✅ elab/grind_bitvec2//instructions: -3.1G (-1.89%)
  • ✅ elab/grind_list2//instructions: -825.2M (-2.10%)
  • 🟥 elab/lift_lets_dag//instructions: +106.9M (+0.88%)
  • ✅ elab/omega_stress//instructions: -60.3M (-1.65%)
  • ✅ elab/simp_bubblesort_256//instructions: -328.5M (-3.28%)
  • and 12 more

Small changes (754✅, 65🟥)

  • ✅ build//task-clock: -51s (-2.42%)
  • ✅ build/module/Init.BinderPredicates//instructions: -30.1M (-1.42%)
  • ✅ build/module/Init.CbvSimproc//instructions: -26.7M (-1.27%)
  • ✅ build/module/Init.Control.Basic//instructions: -33.6M (-1.55%)
  • ✅ build/module/Init.Control.Except//instructions: -22.4M (-1.57%)
  • ✅ build/module/Init.Control.ExceptCps//instructions: -13.1M (-1.18%)
  • ✅ build/module/Init.Control.Lawful.Basic//instructions: -31.8M (-1.48%)
  • ✅ build/module/Init.Control.Lawful.Instances//instructions: -130.2M (-1.93%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Control.Lawful.MonadAttach.Instances//instructions: -18.5M (-1.12%)
  • ✅ build/module/Init.Control.Lawful.MonadLift.Instances//instructions: -12.8M (-1.10%)
  • ✅ build/module/Init.Control.Option//instructions: -9.7M (-1.11%)
  • ✅ build/module/Init.Control.State//instructions: -16.3M (-1.48%)
  • ✅ build/module/Init.Control.StateRef//instructions: -9.0M (-0.98%)
  • ✅ build/module/Init.Conv//instructions: -45.6M (-1.22%)
  • ✅ build/module/Init.Core//instructions: -160.6M (-1.61%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.AC//instructions: -67.3M (-1.75%)
  • ✅ build/module/Init.Data.Array.Attach//instructions: -202.8M (-1.97%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.Basic//instructions: -178.5M (-1.64%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Array.BinSearch//instructions: -52.2M (-0.88%)
  • ✅ build/module/Init.Data.Array.Bootstrap//instructions: -33.5M (-1.44%)
  • and 798 more
  • and 1 hidden

@Kha

Kha commented Aug 29, 2026

Copy link
Copy Markdown
Member Author

!bench mathlib

@leanprover-radar

leanprover-radar commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for leanprover-community/mathlib4-nightly-testing@3495667 against leanprover-community/mathlib4-nightly-testing@78f2465 are in. There are significant results. @Kha

  • 🟥 main exited with code 1

No significant changes detected.

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Aug 29, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Aug 29, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Aug 29, 2026
@Kha Kha added the downstream Request a downstream-lean4 adaptation PR. label Aug 30, 2026
@downstream-lean4 downstream-lean4 Bot mentioned this pull request Aug 30, 2026
Draft
@downstream-lean4

downstream-lean4 Bot commented Aug 30, 2026

Copy link
Copy Markdown

The adaptation PR for this PR is leanprover/downstream-lean4#31.

@Kha
perf: give currRecDepth its own ReaderT layer in CoreM
08499f9 
This PR stops the recursion-depth guard from rebuilding `Core.Context` on every recursive step. Roughly 96% of `Core.Context` reconstructions exist only to bump the depth counter, and each one paid a reference count increment per pointer field.

`withReader` can never reuse the `Context` record, so keeping `currRecDepth` there made every `withIncRecDepth` rebuild it. As its own reader layer the depth is just an extra argument, so a recursion step neither allocates nor touches a reference count. The layer sits inside the `Context` reader so that a bare `read` still resolves to `Context`, and `CoreM.run` gains an initial-depth parameter so nested command elaboration keeps inheriting its caller's depth.

Note this changes `CoreM`'s arity, which is externally observable in LCNF output.
@Kha
Kha force-pushed the core-recdepth-readert branch from f51ba22 to 08499f9 Compare August 31, 2026 16:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR downstream Request a downstream-lean4 adaptation PR. mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Kha @leanprover-radar @leanprover-bot